Problem: f(f(a())) -> c(n__f(g(f(a())))) f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X Proof: Bounds Processor: bound: 2 enrichment: match automaton: final states: {6,5} transitions: f1(35) -> 36* f1(25) -> 26* f1(27) -> 28* f1(33) -> 34* n__f1(17) -> 18* n__f1(19) -> 20* n__f1(9) -> 10* n__f1(11) -> 12* n__f2(49) -> 50* n__f2(51) -> 52* n__f2(41) -> 42* n__f2(43) -> 44* f0(2) -> 5* f0(4) -> 5* f0(1) -> 5* f0(3) -> 5* a0() -> 1* c0(2) -> 2* c0(4) -> 2* c0(1) -> 2* c0(3) -> 2* n__f0(2) -> 3* n__f0(4) -> 3* n__f0(1) -> 3* n__f0(3) -> 3* g0(2) -> 4* g0(4) -> 4* g0(1) -> 4* g0(3) -> 4* activate0(2) -> 6* activate0(4) -> 6* activate0(1) -> 6* activate0(3) -> 6* 1 -> 6,33,11 2 -> 6,25,19 3 -> 6,35,9 4 -> 6,27,17 10 -> 5* 12 -> 5* 18 -> 5* 20 -> 5* 25 -> 41* 26 -> 6* 27 -> 49* 28 -> 6* 33 -> 43* 34 -> 6* 35 -> 51* 36 -> 6* 42 -> 26* 44 -> 34* 50 -> 28,6 52 -> 36,6 problem: Qed